ds:fpf(Id; x.Type). normal-ds{i:l}(ds)  prop{i:l} 

latex

Definitions	x:A. B(x), t  T, prop{i:l}, normal-ds{i:l}(ds), fpf-all(A; eq; f; x,v.P(x;v)), P  Q, x. t(x), x(s)
Lemmas	Id wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, fpf-ap wf, fpf wf